We propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that a broad class of GNNs can be transformed efficiently into a formula, thus significantly improving upon the literature about the logical expressiveness of GNNs. We also show that the satisfiability problem is PSPACE-complete. These results bring together the promise of using standard logical methods for reasoning about GNNs and their properties, particularly in applications such as GNN querying, equivalence checking, etc. We prove that such natural problems can be solved in polynomial space.

Rehabilitation tasks demand robust and accurate trajectory-tracking performance, mainly achieved with parallel robots. In this field, limiting the value of the force exerted on the patient is crucial, especially when an injured limb is involved. In human-robot interaction studies, the admittance controller modifies the location of the robot according to the user efforts driving the end-effector to an arbitrary location within the workspace. However, a parallel robot has singularities within the workspace, making implementing a conventional admittance controller unsafe. Thus, this study proposes an admittance controller that overcomes the limitations of singular configurations by using a real-time singularity avoidance algorithm. The singularity avoidance algorithm modifies the original trajectory based on the actual location of the parallel robot. The complemented admittance controller is applied to a 4 degrees of freedom parallel robot for knee rehabilitation. In this case, the actual location is measured by a 3D tracking system because the location calculated by the forward kinematics is inaccurate in the vicinity of a singularity. The experimental results verify the effectiveness of the proposed admittance controller for safe knee rehabilitation exercises

This paper aims to develop an approach for the reconfiguration of a parallel kinematic manipulator (PKM) with four degrees of freedom (DoF) designed to tackle tasks of diagnosis and rehabilitation in an injured knee. The original layout of the 4-DoF manipulator presents Type-II singular configurations within its workspace. Thus, we proposed to reconfigure the manipulator to avoid such singularities (owing to the Forward Jacobian of the PKM) during typical rehabilitation trajectories. We achieve the reconfiguration of the PKM through a minimization problem where the design variables correspond to the anchoring points of the robot limbs on fixed and mobile platforms. The objective function relies on the minimization of the forces exerted by the actuators for a specific trajectory. The minimization problem considers constraint equations to avoid Type-II singularities, which guarantee the feasibility of the active generalized coordinates for a particular path. To evaluate the proposed conceptual strategy, we build a prototype where reconfiguration occurs by moving the position of the anchoring points to holes bored in the fixed and mobile platforms. Simulations and experiments of several study cases enable testing the strategy performance. The results show that the reconfiguration strategy allows obtaining trajectories having minimum actuation forces without Type-II singularities.

Moreover, PRs have other advantages over their serial counterparts, such as lower weight, higher working speed with high precision, and lower power consumption [1,2]. These advantages, mainly due to the closed kinematic chain architecture, are key aspects that have increased the interest in studying their use in the academic, industrial, and robotics service fields over the last three decades. However, the PR architecture reduces not only the size of the robot workspace but also its kinematic performance, owing to the possible presence of singularities within the workspace. Initially, Gosselin and Angeles [3] studied the singularities of a PR using Jacobian matrices obtained from constraint equations, and classified them into i) inverse kinematic or Type I singularity, where the robot loses at least one degree of freedom (DOF), and ii) Forward Kinematic or Type II singularity, where the PR gains at least one DOF. In particular, Type II singularities could be critical because the mobile platform at the singularity is unable to bear the external forces despite having all the actuators locked (losing control of the PR motion).

Although parallel manipulators (PMs) started with the introduction of architectures with 6 Degrees of Freedom (DoF), a vast number of applications require less than 6 DoF. Consequently, scholars have proposed architectures with 3 DoF and 4 DoF, but relatively few 4 DoF PMs have become prototypes, especially of the two rotation (2R) and two translation (2T) motion types. In this paper, we explain the mechatronics design, prototype and control architecture design of a 4 DoF PM with 2R2T motions. We chose to design a 4 DoF manipulator based on the motion needed to complete the tasks of lower limb rehabilitation. To the author's best knowledge, PMs between 3 and 6 DoF for rehabilitation of lower limbs have not been proposed to date. The developed architecture enhances the three minimum DoF required by adding a 4 DoF which allows combinations of normal or tangential efforts in the joints, or torque acting on the knee. We put forward the inverse and forward displacement equations, describe the prototype, perform the experimental setup, and develop the hardware and control architecture. The tracking accuracy experiments from the proposed controller show that the manipulator can accomplish the required application.

In this paper, we propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that each GNN can be transformed into a formula. We show that the satisfiability problem is decidable. We also discuss some variants that are in PSPACE.

Visual representations of algorithms can improve our understanding of algorithmic concepts and the nature of the underlying problems. Visualizations of the Conflict-Driven Clause Learning algorithm (CDCL) are of high interest, as this is currently the most successful algorithm for solving the propositional satisfiability problem (SAT problem). Despite the complexity of the SAT problem, implementations of CDCL in so-called SAT solvers are successfully used in industrial practice, e.g., in software verification [4], hardware verification [12], product configuration [21], or planning [18]. For satisfiable instances, SAT solvers output a variable assignment which serves as a certificate of satisfiability. Such a certificate can be checked in polynomial time and hence SAT NP.

We propose an automaton model which is a combination of symbolic and register automata, i.e., we enrich symbolic automata with memory. We call such automata Symbolic Register Automata (SRA). SRA extend the expressive power of symbolic automata, by allowing Boolean formulas to be applied not only to the last element read from the input string, but to multiple elements, stored in their registers. SRA also extend register automata, by allowing arbitrary Boolean formulas, besides equality predicates. We study the closure properties of SRA under union, intersection, concatenation, Kleene closure, complement and determinization and show that SRA, contrary to symbolic automata, are not in general closed under complement and they are not determinizable. However, they are closed under these operations when a window operator, quintessential in Complex Event Recognition, is used. We show how SRA can be used in Complex Event Recognition in order to detect patterns upon streams of events, using our framework that provides declarative and compositional semantics, and that allows for a systematic treatment of such automata. We also show how the behavior of SRA, as they consume streams of events, can be given a probabilistic description with the help of prediction suffix trees. This allows us to go one step beyond Complex Event Recognition to Complex Event Forecasting, where, besides detecting complex patterns, we can also efficiently forecast their occurrence.

In most classical models of belief change, epistemic states are represented by theories (AGM) or formulas (Katsuno-Mendelzon) and the new pieces of information by formulas. The Representation Theorem for revision operators says that operators are represented by total preorders. This important representation is exploited by Darwiche and Pearl to shift the notion of epistemic state to a more abstract one, where the paradigm of epistemic state is indeed that of a total preorder over interpretations. In this work, we introduce a 3-valued logic where the formulas can be identified with a generalisation of total preorders of three levels: a ranking function mapping interpretations into the truth values. Then we analyse some sort of changes in this kind of structures and give syntactical characterizations of them.

We use an algebraic viewpoint, namely a matrix framework to deal with the problem of resource allocation under uncertainty in the context of a qualitative approach. Our basic qualitative data are a plausibility relation over the resources, a hierarchical relation over the agents and of course the preference that the agents have over the resources. With this data we propose a qualitative binary relation $\unrhd$ between allocations such that $\mathcal{F}\unrhd \mathcal{G}$ has the following intended meaning: the allocation $\mathcal{F}$ produces more or equal social welfare than the allocation $\mathcal{G}$. We prove that there is a family of allocations which are maximal with respect to $\unrhd$. We prove also that there is a notion of simple deal such that optimal allocations can be reached by sequences of simple deals. Finally, we introduce some mechanism for discriminating {optimal} allocations.